\begin{tabbing} onceR\=\{\$a:ut2, \$done:ut2\}\+ \\[0ex]($i$) \-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Rlist(cons(\=Rpre(\=$i$;\+\+ \\[0ex]fpf{-}single(mkid\{\$done:ut2\}; $\mathbb{B}$); \\[0ex]mkid\{\$a:ut2\}; \\[0ex]unit{-}fps; \\[0ex]($\lambda$$s$.$\neg_{b}$es{-}state{-}ap($s$; mkid\{\$done:ut2\}))); \-\\[0ex]cons(\=Rinit($i$; $\mathbb{B}$; mkid\{\$done:ut2\}; (inl ff ));\+ \\[0ex]cons(\=Reffect(\=$i$;\+\+ \\[0ex]fpf{-}single(mkid\{\$done:ut2\}; $\mathbb{B}$); \\[0ex]locl(mkid\{\$a:ut2\}); \\[0ex]p{-}outcome(unit{-}fps); \\[0ex]mkid\{\$done:ut2\}; \\[0ex](inl ($\lambda$$s$,$v$. tt) )); \-\\[0ex]cons(\=Rframe(\=$i$; $\mathbb{B}$; mkid\{\$done:ut2\}; cons(locl(mkid\{\$a:ut2\}); [])\+\+ \\[0ex]); \-\\[0ex][]))))) \-\-\-\- \end{tabbing}